$\forall$$T$:Type, $v$:$T$, $x$, $i$:Id. AtomFree(Type;$T$) $\Rightarrow$ $\vdash$${\it es}$.@$i$ $x$ initially $v$:$T$